Inference at * 
Iof proof for Lemma list extensionality:


  T:Type, a, b:(T List). (||a|| = ||b||)  (i:. (i < ||a||)  (a[i] = b[i]))  (a = b) 

latex

 by ((UnivCD) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n
C)) (first_tok SupInf:t) inil_term))) 

latex

C1: 

C1: 1. T : Type
C1: 2. a : T List
C1: 3. b : T List
C1: 4. ||a|| = ||b||
C1: 5. i:. (i < ||a||)  (a[i] = b[i])
C1:   a = b
C.

Definitions	, t  T, P  Q, x:A. B(x),
Lemmas	length wf1, select wf, nat wf